r:CRng, a, b:|r|. (a * b) = (b * a)  |r| 

latex

Up	rings 1
Definitions of Statement	Rng, CRng, rxmn
Definitions	IMonoid, t  T, IAbMonoid, x f y, x:A. B(x), t.2, t.1, , P & Q, Mon, AbMon, rxmn, *, |g|
Lemmas	crng wf, abmonoid wf, comm wf, grp id wf, grp op wf, grp car wf, monoid p wf, mul mon of rng wf b, abmonoid comm